Require Import Notations.
Require Import Ltac.
Require Import Datatypes.
Require Import Logic.
Require Coq.Init.Nat.

Open Scope nat_scope.

Theorem lt_S: forall n p: nat, n < p -> n < S p.
Proof.
  intros n p H.
  unfold lt.
  apply le_S.
  trivial.
Qed.